\begin{tabbing}
es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$$\in$fpf{-}domain(${\it ds}$).let $T$ = ${\it ds}$($x$) in vartype($i$;$x$) $\subseteq\rho$ $T$\+
\\[0ex]\& $\forall$\=$k$$\in$fpf{-}domain(${\it da}$).\+
\\[0ex]let $T$ = ${\it da}$($k$) in $\forall$$e$:E. loc($e$) $=$ $i$ $\vee$ isrcv($e$) $\Rightarrow$ kind($e$) $=$ $k$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$
\-\-
\end{tabbing}